$\vdash$  $\forall$$A$:Type, $f$:($A$$\rightarrow$($A$ + Top)). $f$\^{}1 = $f$